with System;

package body Stack
with SPARK_Mode
is

   pragma Suppress (All_Checks);

   ------------
   -- Calloc --
   ------------

   procedure Calloc
      (Size : Integer)
      with SPARK_Mode => Off
   is
      procedure Print (Str : System.Address)
         with
         Import,
         Convention => C,
         External_Name => "print_stack";

         Buf : Buffer := Alloc (Size) & Character'Val (0);
   begin
      Print (Buf'Address);
   end Calloc;

   procedure Ralloc
   is
      R : constant Integer := 0;
      B : Buffer := Recursive_Alloc (R);
      pragma Unreferenced (B);
   begin
      null;
   end Ralloc;

   -----------
   -- Alloc --
   -----------

   function Alloc
      (Size : Integer)
      return Buffer
   is
      Buf : constant Buffer (1 .. Size) := (others => '0');
   begin
      return Buf;
   end Alloc;

   function Recursive_Alloc (Round : Integer) return Buffer
   is
      procedure Print (R : Integer)
         with
         Import,
         Convention => C,
         External_Name => "print_recursion";

         Buf : constant Buffer (1 .. 256) := (others => '0');
   begin
      Print (Round);
      if Round < 10 then
         return Buf & Recursive_Alloc (Round + 1);
      else
         return Buf;
      end if;
   end Recursive_Alloc;

   procedure Salloc
   is
      S : constant Integer := 16;
      B : Buffer := Stage_1 (S);
      pragma Unreferenced (B);
   begin
      Print_Stage (0);
   end Salloc;

   function Stage_1 (
      Size : Integer
      ) return Buffer
   is
      Buf : Buffer (1 .. Size) := (others => '0');
   begin
      Print_Stage (1);
      declare
         Buf_2 : constant Buffer := Stage_2 (Size);
      begin
         Buf := Buf_2;
      end;
      return Buf;
   end Stage_1;

   function Stage_2 (
      Size : Integer
      ) return Buffer
   is
      Buf : Buffer (1 .. Size);
   begin
      Print_Stage (2);
      declare
         Buf2 : constant Buffer := Stage_3 (Size);
      begin
         Buf := Buf2;
      end;
      return Buf;
   end Stage_2;

   function Stage_3 (
      Size : Integer
      ) return Buffer
   is
      Buf : constant Buffer (1 .. Size) := (others => '3');
   begin
      Print_Stage (3);
      return Buf;
   end Stage_3;

end Stack;
